Nuprl Lemma : comb_for_tree_leaf_wf2
4,23
postcript
pdf
(
E
,
x
,
z
. tree_leaf(
x
))
E
:Type
E
True
Tree(
E
)
latex
Definitions
T
,
x
:
A
.
B
(
x
)
,
t
T
,
True
Lemmas
true
wf
,
squash
wf
,
tree
leaf
wf2
origin
E,x,z. tree_leaf(x)) 
E:Type
E
TrueTree(E) E,x,z. tree_leaf(x)) E:TypeETrueTree(E) T
x:A. B(x) T